1 /-
2 Copyright (c) 2019 Kenny Lau. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Kenny Lau
5
6 Integral closure of a subring.
7 -/
8
9 import ring_theory.adjoin linear_algebra.finsupp
src └────────────────┘ └────────────────────┘
10
11 universes u v
12
13 open_locale classical
14 open polynomial submodule
15
16 section
17 variables (R : Type u) {A : Type v}
18 variables [comm_ring R] [comm_ring A]
19 variables [algebra R A]
id └─────┘
src └─────┘
typ └─────┘
doc └─────┘
20
21 def is_integral (x : A) : Prop :=
id ┴
typ ┴
22 ∃ p : polynomial R, monic p ∧ aeval R A x p = 0
id ┴ └────────┘ ┴┴ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
src ┴ └────────┘ ┴ └───┘ ┴ └───┘ ┴
typ ┴ └────────┘ ┴┴ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
doc └────────┘ └───┘ └───┘
23
24 variables {R}
25 theorem is_integral_algebra_map {x : R} : is_integral R (algebra_map A x) :=
id ┴ └─────────┘ ┴ └─────────┘ ┴ ┴
src └─────────┘ └─────────┘
typ ┴ └─────────┘ ┴ └─────────┘ ┴ ┴
26 ⟨X - C x, monic_X_sub_C _,
id ┴ ┴ ┴ ┴ └───────────┘
src ┴ ┴ ┴ └───────────┘
typ ┴ ┴ ┴ ┴ └───────────┘
doc ┴ ┴
27 by rw [alg_hom.map_sub, aeval_def, aeval_def, eval₂_X, eval₂_C, sub_self]⟩
id └─────────────┘ └───────┘ └───────┘ └─────┘ └─────┘ └──────┘
src └──┘└─────────────┘└┘└───────┘└┘└───────┘└┘└─────┘└┘└─────┘└┘└──────┘┴
typ └──┘└─────────────┘└┘└───────┘└┘└───────┘└┘└─────┘└┘└─────┘└┘└──────┘┴
doc └──┘ └┘ └┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ └┘ └┘ ┴
st └──────────────────┘└─────────┘└─────────┘└───────┘└───────┘└────────┘┴
28
29 theorem is_integral_of_subring {x : A} (T : set R) [is_subring T]
id ┴ └─┘ ┴ └────────┘ ┴
src └─┘ └────────┘
typ ┴ └─┘ ┴ └────────┘ ┴
doc └────────┘
30 (hx : is_integral T (algebra.comap.to_comap T R A x)) : is_integral R (x : A) :=
id └─────────┘ ┴ └────────────────────┘ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴
src └─────────┘ └────────────────────┘ └─────────┘
typ └─────────┘ ┴ └────────────────────┘ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴
31 let ⟨p, hpm, hpx⟩ := hx in
id └─┘ ┴ └─┘ └─┘ └┘
typ └─┘ ┴ └─┘ └─┘ └┘
32 ⟨⟨p.support, λ n, (p.to_fun n).1,
id └──────┘ ┴ └─────┘ ┴ ┴
src └──────┘ └─────┘ ┴
typ └──────┘ ┴ └─────┘ ┴ ┴
33 λ n, finsupp.mem_support_iff.trans (not_iff_not_of_iff
id ┴ └─────────────────────┘└────┘ └────────────────┘
src └─────────────────────┘└────┘ └────────────────┘
typ ┴ └─────────────────────┘└────┘ └────────────────┘
34 ⟨λ H, have _ := congr_arg subtype.val H, this,
id ┴ └───────┘ └─────────┘ ┴ └──┘
src └───────┘ └─────────┘
typ ┴ └───────┘ └─────────┘ ┴ └──┘
35 λ H, subtype.eq H⟩)⟩,
id ┴ └────────┘ ┴
src └────────┘
typ ┴ └────────┘ ┴
36 have _ := congr_arg subtype.val hpm, this, hpx⟩
id └───────┘ └─────────┘ └──┘
src └───────┘ └─────────┘
typ └───────┘ └─────────┘ └──┘
37
38 theorem is_integral_iff_is_integral_closure_finite {r : A} :
id ┴
typ ┴
39 is_integral R r ↔ ∃ s : set R, s.finite ∧
id └─────────┘ ┴ ┴ ┴ ┴ └─┘ ┴┴ ┴└─────┘ ┴
src └─────────┘ ┴ ┴ └─┘ ┴ └─────┘ ┴
typ └─────────┘ ┴ ┴ ┴ ┴ └─┘ ┴┴ ┴└─────┘ ┴
doc └─────┘
40 is_integral (ring.closure s) (algebra.comap.to_comap (ring.closure s) R A r) :=
id └─────────┘ └──────────┘ ┴ └────────────────────┘ └──────────┘ ┴ ┴ ┴ ┴
src └─────────┘ └──────────┘ └────────────────────┘ └──────────┘
typ └─────────┘ └──────────┘ ┴ └────────────────────┘ └──────────┘ ┴ ┴ ┴ ┴
41 begin
st └─────
42 split; intro hr,
src └───┘ └──────┘
typ └───┘ └──────┘
doc └───┘ └──────┘
txt └───┘ └──────┘
par └───┘ └──────┘
pid └─┘
st ────────────────┘└─
43 { rcases hr with ⟨p, hmp, hpr⟩,
id └┘
src └─────┘ └─────────────────┘
typ └─────┘└┘└─────────────────┘
doc └─────┘ └─────────────────┘
txt └─────┘ └─────────────────┘
par └─────┘ └─────────────────┘
pid ┴ └─────────────────┘
st ───┘└──────────────────────────┘└─
44 exact ⟨_, set.finite_mem_finset _, p.restriction, subtype.eq hmp, hpr⟩ },
id └───────────────────┘ └───────────┘ └────────┘ └─┘ └─┘
src └────┘ └─┘└───────────────────┘└──┘└───────────┘└┘└────────┘┴ └┘ └┘
typ └────┘ └─┘└───────────────────┘└──┘└───────────┘└┘└────────┘┴└─┘└┘└─┘└┘
doc └────┘ └─┘ └──┘└───────────┘└┘ ┴ └┘ └┘
txt └────┘ └─┘ └──┘ └┘ ┴ └┘ └┘
par └────┘ └─┘ └──┘ └┘ ┴ └┘ └┘
pid ┴ └─┘ └──┘ └┘ ┴ └┘ ┴┴
st ──────────────────────────────────────────────────────────────────────────┘└┘└
45 rcases hr with ⟨s, hs, hsr⟩,
id └┘
src └─────┘ └────────────────┘
typ └─────┘└┘└────────────────┘
doc └─────┘ └────────────────┘
txt └─────┘ └────────────────┘
par └─────┘ └────────────────┘
pid ┴ └────────────────┘
st ────────────────────────────┘└─
46 exact is_integral_of_subring _ hsr
id └────────────────────┘ └─┘
src └────┘└────────────────────┘└─┘ ┴
typ └────┘└────────────────────┘└─┘└─┘┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ────────────────────────────────────┘
47 end
st └─┘
48
49 theorem fg_adjoin_singleton_of_integral (x : A) (hx : is_integral R x) :
id ┴ └─────────┘ ┴ ┴
src └─────────┘
typ ┴ └─────────┘ ┴ ┴
50 (algebra.adjoin R ({x} : set A) : submodule R A).fg :=
id └────────────┘ ┴ ┴┴ └─┘ ┴ └───────┘ ┴ ┴ └┘
src └────────────┘ ┴ └─┘ └───────┘ └┘
typ └────────────┘ ┴ ┴┴ └─┘ ┴ └───────┘ ┴ ┴ └┘
doc └───────┘
51 begin
st └─────
52 rcases hx with ⟨f, hfm, hfx⟩,
id └┘
src └─────┘ └─────────────────┘
typ └─────┘└┘└─────────────────┘
doc └─────┘ └─────────────────┘
txt └─────┘ └─────────────────┘
par └─────┘ └─────────────────┘
pid ┴ └─────────────────┘
st ─────────────────────────────┘└─
53 existsi finset.image ((^) x) (finset.range (nat_degree f + 1)),
id └──────────┘ ┴ ┴ └──────────┘ └────────┘ ┴ ┴
src └──────┘└──────────┘┴ ┴└─┘ └┘ └──────────┘┴ └────────┘┴ ┴┴└──┘
typ └──────┘└──────────┘┴ ┴└─┘┴└┘ └──────────┘┴ └────────┘┴┴┴┴└──┘
doc └──────┘└──────────┘┴ └─┘ └┘ └──────────┘┴ └────────┘┴ ┴ └──┘
txt └──────┘ ┴ └─┘ └┘ ┴ ┴ ┴ └──┘
par └──────┘ ┴ └─┘ └┘ ┴ ┴ ┴ └──┘
pid ┴ ┴ └─┘ └┘ ┴ ┴ ┴ └──┘
st ───────────────────────────────────────────────────────────────┘└─
54 apply le_antisymm,
id └─────────┘
src └────┘└─────────┘
typ └────┘└─────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────┘└─
55 { rw span_le, intros s hs, rw finset.mem_coe at hs,
id └─────┘ └────────────┘
src └─┘└─────┘ └─────────┘ └─┘└────────────┘└────┘
typ └─┘└─────┘ └─────────┘ └─┘└────────────┘└────┘
doc └─┘ └─────────┘ └─┘ └────┘
txt └─┘ └─────────┘ └─┘ └────┘
par └─┘ └─────────┘ └─┘ └────┘
pid ┴ └───┘ ┴ └────┘
st ───┘└────────┘└───────────┘└───────────────────────┘└─
56 rcases finset.mem_image.1 hs with ⟨k, hk, rfl⟩, clear hk,
id └──────────────┘ └┘
src └─────┘└──────────────┘└─┘ └────────────────┘ └──────┘
typ └─────┘└──────────────┘└─┘└┘└────────────────┘ └──────┘
doc └─────┘ └─┘ └────────────────┘ └──────┘
txt └─────┘ └─┘ └────────────────┘ └──────┘
par └─────┘ └─┘ └────────────────┘ └──────┘
pid ┴ └─┘ └────────────────┘ └─┘
st ─────────────────────────────────────────────────┘└────────┘└─
57 exact is_submonoid.pow_mem (algebra.subset_adjoin (set.mem_singleton _)) },
id └──────────────────┘ └───────────────────┘ └───────────────┘
src └────┘└──────────────────┘┴ └───────────────────┘┴ └───────────────┘└───┘
typ └────┘└──────────────────┘┴ └───────────────────┘┴ └───────────────┘└───┘
doc └────┘└──────────────────┘┴ ┴ └───┘
txt └────┘ ┴ ┴ └───┘
par └────┘ ┴ ┴ └───┘
pid ┴ ┴ ┴ └──┘┴
st ────────────────────────────────────────────────────────────────────────────┘└┘└
58 intros r hr, change r ∈ algebra.adjoin R ({x} : set A) at hr,
id ┴ ┴ └────────────┘ ┴ ┴ └─┘ ┴
src └─────────┘ └─────┘ ┴┴┴└────────────┘┴ ┴ ┴└───┘└─┘┴ └─────┘
typ └─────────┘ └─────┘┴┴┴┴└────────────┘┴┴┴ ┴└───┘└─┘┴┴└─────┘
doc └─────────┘ └─────┘ ┴ ┴ ┴ ┴ └───┘ ┴ └─────┘
txt └─────────┘ └─────┘ ┴ ┴ ┴ ┴ └───┘ ┴ └─────┘
par └─────────┘ └─────┘ ┴ ┴ ┴ ┴ └───┘ ┴ └─────┘
pid └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴┴└───┘
st ────────────┘└───────────────────────────────────────────────┘└─
59 rw algebra.adjoin_singleton_eq_range at hr, rcases hr with ⟨p, rfl⟩,
id └───────────────────────────────┘ └┘
src └─┘└───────────────────────────────┘└────┘ └─────┘ └────────────┘
typ └─┘└───────────────────────────────┘└────┘ └─────┘└┘└────────────┘
doc └─┘ └────┘ └─────┘ └────────────┘
txt └─┘ └────┘ └─────┘ └────────────┘
par └─┘ └────┘ └─────┘ └────────────┘
pid ┴ └────┘ ┴ └────────────┘
st ───────────────────────────────────────────┘└───────────────────────┘└─
60 rw ← mod_by_monic_add_div p hfm,
id └──────────────────┘ ┴ └─┘
src └───┘└──────────────────┘┴ ┴
typ └───┘└──────────────────┘┴┴┴└─┘
doc └───┘ ┴ ┴
txt └───┘ ┴ ┴
par └───┘ ┴ ┴
pid └─┘ ┴ ┴
st ────────────────────────────────┘└─
61 rw [alg_hom.map_add, alg_hom.map_mul, hfx, zero_mul, add_zero],
id └─────────────┘ └─────────────┘ └─┘ └──────┘ └──────┘
src └──┘└─────────────┘└┘└─────────────┘└┘ └┘└──────┘└┘└──────┘┴
typ └──┘└─────────────┘└┘└─────────────┘└┘└─┘└┘└──────┘└┘└──────┘┴
doc └──┘ └┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ └┘ ┴
st ────────────────────┘└───────────────┘└───┘└────────┘└────────┘└──
62 have : degree (p %ₘ f) ≤ degree f := degree_mod_by_monic_le p hfm,
id ┴ └┘ ┴ └────┘ ┴ └────────────────────┘ ┴ └─┘
src └─────┘ ┴ ┴└┘┴ └┘┴┴└────┘┴ └──┘└────────────────────┘┴ ┴
typ └─────┘ ┴ ┴┴└┘┴ └┘┴┴└────┘┴┴└──┘└────────────────────┘┴┴┴└─┘
doc └─────┘ ┴ ┴└┘┴ └┘ ┴└────┘┴ └──┘ ┴ ┴
txt └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ └──┘ ┴ ┴
par └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ └──┘ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ └┘ ┴ ┴ └──┘ ┴ ┴
st ──────────────────────────────────────────────────────────────────┘└─
63 generalize_hyp : p %ₘ f = q at this ⊢,
id ┴ ┴
src └───────────────┘ ┴ ┴ ┴ ┴ └────────┘
typ └───────────────┘┴┴ ┴┴┴ ┴ └────────┘
doc └───────────────┘ ┴ ┴ ┴ ┴ └────────┘
txt └───────────────┘ ┴ ┴ ┴ ┴ └────────┘
par └───────────────┘ ┴ ┴ ┴ ┴ └────────┘
pid ┴┴┴ ┴ ┴ ┴ ┴ └────────┘
st ──────────────────────────────────────┘└─
64 rw [← sum_C_mul_X_eq q, aeval_def, eval₂_sum, finsupp.sum, mem_coe],
id └────────────┘ ┴ └───────┘ └───────┘ └─────────┘ └─────┘
src └────┘└────────────┘┴ └┘└───────┘└┘└───────┘└┘└─────────┘└┘└─────┘┴
typ └────┘└────────────┘┴┴└┘└───────┘└┘└───────┘└┘└─────────┘└┘└─────┘┴
doc └────┘ ┴ └┘ └┘ └┘└─────────┘└┘ ┴
txt └────┘ ┴ └┘ └┘ └┘ └┘ ┴
par └────┘ ┴ └┘ └┘ └┘ └┘ ┴
pid └──┘ ┴ └┘ └┘ └┘ └┘ ┴
st ───────────────────────┘└─────────┘└─────────┘└───────────┘└───────┘└──
65 refine sum_mem _ (λ k hkq, _),
id └─────┘
src └─────┘└─────┘└─┘ └────────┘
typ └─────┘└─────┘└─┘ └────────┘
doc └─────┘ └─┘ └────────┘
txt └─────┘ └─┘ └────────┘
par └─────┘ └─┘ └────────┘
pid ┴ └─┘ └────────┘
st ──────────────────────────────┘└─
66 rw [eval₂_mul, eval₂_C, eval₂_pow, eval₂_X, ← algebra.smul_def],
id └───────┘ └─────┘ └───────┘ └─────┘ └──────────────┘
src └──┘└───────┘└┘└─────┘└┘└───────┘└┘└─────┘└──┘└──────────────┘┴
typ └──┘└───────┘└┘└─────┘└┘└───────┘└┘└─────┘└──┘└──────────────┘┴
doc └──┘ └┘ └┘ └┘ └──┘ ┴
txt └──┘ └┘ └┘ └┘ └──┘ ┴
par └──┘ └┘ └┘ └┘ └──┘ ┴
pid └┘ └┘ └┘ └┘ └──┘ ┴
st ──────────────┘└───────┘└─────────┘└───────┘└──────────────────┘└──
67 refine smul_mem _ _ (subset_span _),
id └──────┘ └─────────┘
src └─────┘└──────┘└───┘ └─────────┘└─┘
typ └─────┘└──────┘└───┘ └─────────┘└─┘
doc └─────┘ └───┘ └─┘
txt └─────┘ └───┘ └─┘
par └─────┘ └───┘ └─┘
pid ┴ └───┘ └─┘
st ────────────────────────────────────┘└─
68 rw finset.mem_coe, refine finset.mem_image.2 ⟨_, _, rfl⟩,
id └────────────┘ └──────────────┘ └─┘
src └─┘└────────────┘ └─────┘└──────────────┘└─┘ └────┘└─┘┴
typ └─┘└────────────┘ └─────┘└──────────────┘└─┘ └────┘└─┘┴
doc └─┘ └─────┘ └─┘ └────┘ ┴
txt └─┘ └─────┘ └─┘ └────┘ ┴
par └─┘ └─────┘ └─┘ └────┘ ┴
pid ┴ ┴ └─┘ └────┘ ┴
st ──────────────────┘└─────────────────────────────────────┘└─
69 rw [finset.mem_range, nat.lt_succ_iff], refine le_of_not_lt (λ hk, _),
id └──────────────┘ └─────────────┘ └──────────┘
src └──┘└──────────────┘└┘└─────────────┘┴ └─────┘└──────────┘┴ └─────┘
typ └──┘└──────────────┘└┘└─────────────┘┴ └─────┘└──────────┘┴ └─────┘
doc └──┘ └┘ ┴ └─────┘ ┴ └─────┘
txt └──┘ └┘ ┴ └─────┘ ┴ └─────┘
par └──┘ └┘ ┴ └─────┘ ┴ └─────┘
pid └┘ └┘ ┴ ┴ ┴ └─────┘
st ─────────────────────┘└───────────────┘└──────────────────────────────┘└─
70 rw [degree_le_iff_coeff_zero] at this,
id └──────────────────────┘
src └──┘└──────────────────────┘└───────┘
typ └──┘└──────────────────────┘└───────┘
doc └──┘ └───────┘
txt └──┘ └───────┘
par └──┘ └───────┘
pid └┘ ┴└──────┘
st ─────────────────────────────┘┴└──────┘└─
71 rw [finsupp.mem_support_iff] at hkq, apply hkq, apply this,
id └─────────────────────┘
src └──┘└─────────────────────┘└──────┘ └────┘ └────┘
typ └──┘└─────────────────────┘└──────┘ └────┘ └────┘
doc └──┘ └──────┘ └────┘ └────┘
txt └──┘ └──────┘ └────┘ └────┘
par └──┘ └──────┘ └────┘ └────┘
pid └┘ ┴└─────┘ ┴ ┴
st ────────────────────────────┘┴└─────┘└─────────┘└──────────┘└─
72 exact lt_of_le_of_lt degree_le_nat_degree (with_bot.coe_lt_coe.2 hk)
id └────────────┘ └──────────────────┘ └─────────────────┘ └┘
src └────┘└────────────┘┴└──────────────────┘┴ └─────────────────┘└─┘ └┘
typ └────┘└────────────┘┴└──────────────────┘┴ └─────────────────┘└─┘└┘└┘
doc └────┘ ┴ ┴ └─┘ └┘
txt └────┘ ┴ ┴ └─┘ └┘
par └────┘ ┴ ┴ └─┘ └┘
pid ┴ ┴ ┴ └─┘ ┴┴
st ──────────────────────────────────────────────────────────────────────┘
73 end
st └─┘
74
75 theorem fg_adjoin_of_finite {s : set A} (hfs : s.finite)
id └─┘ ┴ ┴└─────┘
src └─┘ └─────┘
typ └─┘ ┴ ┴└─────┘
doc └─────┘
76 (his : ∀ x ∈ s, is_integral R x) : (algebra.adjoin R s : submodule R A).fg :=
id ┴ ┴ └─────────┘ ┴ ┴ └────────────┘ ┴ ┴ └───────┘ ┴ ┴ └┘
src ┴ └─────────┘ └────────────┘ └───────┘ └┘
typ ┴ ┴ └─────────┘ ┴ ┴ └────────────┘ ┴ ┴ └───────┘ ┴ ┴ └┘
doc └───────┘
77 set.finite.induction_on hfs (λ _, ⟨finset.singleton 1, le_antisymm
id └─────────────────────┘ └─┘ ┴ └──────────────┘ └─────────┘
src └─────────────────────┘ └──────────────┘ └─────────┘
typ └─────────────────────┘ └─┘ ┴ └──────────────┘ └─────────┘
doc └──────────────┘
78 (span_le.2 $ set.singleton_subset_iff.2 $ is_submonoid.one_mem _)
id └─────┘┴ └──────────────────────┘┴ └──────────────────┘
src └─────┘┴ └──────────────────────┘┴ └──────────────────┘
typ └─────┘┴ └──────────────────────┘┴ └──────────────────┘
79 (show ring.closure _ ⊆ _, by rw set.union_empty; exact
id └──────────┘ ┴ └─────────────┘
src └──────────┘ ┴ └─┘└─────────────┘ └─────
typ └──────────┘ ┴ └─┘└─────────────┘ └─────
doc └─┘ └─────
txt └─┘ └─────
par └─┘ └─────
pid ┴ └
st └──────────────────────────
80 set.subset.trans (ring.closure_subset (set.subset.refl _))
id └──────────────┘ └─────────────────┘ └─────────────┘
src ───┘└──────────────┘┴ └─────────────────┘┴ └─────────────┘└────
typ ───┘└──────────────┘┴ └─────────────────┘┴ └─────────────┘└────
doc ───┘ ┴ ┴ └────
txt ───┘ ┴ ┴ └────
par ───┘ ┴ ┴ └────
pid ───┘ ┴ ┴ └────
st ───────────────────────────────────────────────────────────────
81 (λ y ⟨x, hx⟩, hx ▸ mul_one (algebra_map A x) ▸ algebra.smul_def x (1:A) ▸ (mem_coe _).2
id ┴ └┘ ┴ └─────┘ └─────────┘ └──────────────┘ ┴ └─────┘
src ───┘ └──┘ └┘ └─┘ ┴┴┴└─────┘┴ └─────────┘┴ ┴ └┘ ┴└──────────────┘┴ ┴ └┘ └┘ ┴ └─────┘└─────
typ ───┘ └──┘┴└┘└┘└─┘ ┴┴┴└─────┘┴ └─────────┘┴ ┴ └┘ ┴└──────────────┘┴ ┴ └┘┴└┘ ┴ └─────┘└─────
doc ───┘ └──┘ └┘ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └┘ ┴ └─────
txt ───┘ └──┘ └┘ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └┘ ┴ └─────
par ───┘ └──┘ └┘ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └┘ ┴ └─────
pid ───┘ └──┘ └┘ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └┘ ┴ └─────
st ────────────────────────────────────────────────────────────────────────────────────────────
82 (submodule.smul_mem _ x $ subset_span $ or.inl rfl)))⟩)
id └────────────────┘ └─────────┘ └────┘ └─┘
src ─────┘ └────────────────┘└─┘ ┴ ┴└─────────┘┴ ┴└────┘┴└─┘└┘
typ ─────┘ └────────────────┘└─┘ ┴ ┴└─────────┘┴ ┴└────┘┴└─┘└┘
doc ─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ └┘
txt ─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ └┘
par ─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ └┘
pid ─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ └┘
st ─────────────────────────────────────────────────────────┘
83 (λ a s has hs ih his, by rw [← set.union_singleton, algebra.adjoin_union_coe_submodule]; exact
id ┴ ┴ └─┘ └┘ └┘ └─┘ └─────────────────┘ └────────────────────────────────┘
src └────┘└─────────────────┘└┘└────────────────────────────────┘┴ └─────
typ ┴ ┴ └─┘ └┘ └┘ └─┘ └────┘└─────────────────┘└┘└────────────────────────────────┘┴ └─────
doc └────┘ └┘ ┴ └─────
txt └────┘ └┘ ┴ └─────
par └────┘ └┘ ┴ └─────
pid └──┘ └┘ ┴ └
st └────────────────────────┘└──────────────────────────────────┘┴└───────
84 fg_mul _ _ (ih $ λ i hi, his i $ set.mem_insert_of_mem a hi)
id └────┘ └┘ └───────────────────┘
src ─┘└────┘└───┘ ┴ ┴ └─────┘ ┴ ┴ ┴└───────────────────┘┴ ┴ └─
typ ─┘└────┘└───┘ └┘┴ ┴ └─────┘ ┴ ┴ ┴└───────────────────┘┴ ┴ └─
doc ─┘ └───┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └─
txt ─┘ └───┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └─
par ─┘ └───┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └─
pid ─┘ └───┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └─
st ───────────────────────────────────────────────────────────────
85 (fg_adjoin_singleton_of_integral _ $ his a $ set.mem_insert a s)) his
id └─────────────────────────────┘ └─┘ └────────────┘ ┴ ┴ └─┘
src ───┘ └─────────────────────────────┘└─┘ ┴ ┴ ┴ ┴└────────────┘┴ ┴ ┴
typ ───┘ └─────────────────────────────┘└─┘ ┴└─┘┴ ┴ ┴└────────────┘┴┴┴┴┴ └─┘
doc ───┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt ───┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par ───┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid ───┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────────┘
86
87 theorem is_integral_of_noetherian' (H : is_noetherian R A) (x : A) :
id └───────────┘ ┴ ┴ ┴
src └───────────┘
typ └───────────┘ ┴ ┴ ┴
88 is_integral R x :=
id └─────────┘ ┴ ┴
src └─────────┘
typ └─────────┘ ┴ ┴
89 begin
st └─────
90 let leval : @linear_map R (polynomial R) A _ _ _ _ _ := (aeval R A x).to_linear_map,
id └────────┘ └────────┘ ┴ ┴ └───┘ ┴ ┴ ┴
src └──────────┘ └────────┘┴ ┴ └────────┘┴ └┘ └────────────┘ └───┘┴ ┴ ┴ └─────────────┘
typ └──────────┘ └────────┘┴ ┴ └────────┘┴┴└┘┴└────────────┘ └───┘┴┴┴┴┴┴└─────────────┘
doc └──────────┘ ┴ ┴ └────────┘┴ └┘ └────────────┘ └───┘┴ ┴ ┴ └─────────────┘
txt └──────────┘ ┴ ┴ ┴ └┘ └────────────┘ ┴ ┴ ┴ └─────────────┘
par └──────────┘ ┴ ┴ ┴ └┘ └────────────┘ ┴ ┴ ┴ └─────────────┘
pid └───────┘└─┘ ┴ ┴ ┴ └┘ └────────┘└──┘ ┴ ┴ ┴ └────────────┘┴
st ────────────────────────────────────────────────────────────────────────────────────┘└─
91 let D : ℕ → submodule R A := λ n, (degree_le R n).map leval,
id └───────┘ ┴ ┴ └───────┘ ┴ └───┘
src └──────┘ ┴ ┴└───────┘┴ ┴ └──┘ └──┘ └───────┘┴ ┴ └────┘
typ └──────┘ ┴ ┴└───────┘┴┴┴┴└──┘ └──┘ └───────┘┴┴┴ └────┘└───┘
doc └──────┘ ┴ ┴└───────┘┴ ┴ └──┘ └──┘ └───────┘┴ ┴ └────┘
txt └──────┘ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ └────┘
par └──────┘ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ └────┘
pid └───┘└─┘ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ └────┘
st ────────────────────────────────────────────────────────────┘└─
92 let M := well_founded.min (is_noetherian_iff_well_founded.1 H)
id └──────────────┘ └────────────────────────────┘ ┴
src └───────┘└──────────────┘┴ └────────────────────────────┘└─┘ └─
typ └───────┘└──────────────┘┴ └────────────────────────────┘└─┘┴└─
doc └───────┘└──────────────┘┴ └─┘ └─
txt └───────┘ ┴ └─┘ └─
par └───────┘ ┴ └─┘ └─
pid └───┘┴└─┘ ┴ └─┘ └─
st ─────────────────────────────────────────────────────────────────
93 (set.range D) ⟨_, ⟨0, rfl⟩⟩,
id └───────┘ ┴ └─┘
src ───┘ └───────┘┴ └┘ └─┘ └─┘└─┘└┘
typ ───┘ └───────┘┴┴└┘ └─┘ └─┘└─┘└┘
doc ───┘ └───────┘┴ └┘ └─┘ └─┘ └┘
txt ───┘ ┴ └┘ └─┘ └─┘ └┘
par ───┘ ┴ └┘ └─┘ └─┘ └┘
pid ───┘ ┴ └┘ └─┘ └─┘ └┘
st ──────────────────────────────┘└─
94 have HM : M ∈ set.range D := well_founded.min_mem _ _ _,
id ┴ ┴ └───────┘ ┴ └──────────────────┘
src └────────┘ ┴┴┴└───────┘┴ └──┘└──────────────────┘└────┘
typ └────────┘┴┴┴┴└───────┘┴┴└──┘└──────────────────┘└────┘
doc └────────┘ ┴ ┴└───────┘┴ └──┘ └────┘
txt └────────┘ ┴ ┴ ┴ └──┘ └────┘
par └────────┘ ┴ ┴ ┴ └──┘ └────┘
pid └─────┘└─┘ ┴ ┴ ┴ └──┘ └────┘
st ────────────────────────────────────────────────────────┘└─
95 cases HM with N HN,
id └┘
src └────┘ └────────┘
typ └────┘└┘└────────┘
doc └────┘ └────────┘
txt └────┘ └────────┘
par └────┘ └────────┘
pid ┴ └────────┘
st ───────────────────┘└─
96 have HM : ¬M < D (N+1) := well_founded.not_lt_min
id ┴┴ ┴ ┴ ┴┴ └─────────────────────┘
src └────────┘┴ ┴┴┴ ┴ ┴└────┘└─────────────────────┘└
typ └────────┘┴┴┴┴┴┴┴ ┴┴└────┘└─────────────────────┘└
doc └────────┘ ┴ ┴ ┴ └────┘ └
txt └────────┘ ┴ ┴ ┴ └────┘ └
par └────────┘ ┴ ┴ ┴ └────┘ └
pid └─────┘└─┘ ┴ ┴ ┴ └┘└──┘ └
st ────────────────────────────────────────────────────
97 (is_noetherian_iff_well_founded.1 H) (set.range D) _ ⟨N+1, rfl⟩,
id └────────────────────────────┘ ┴ └───────┘ ┴ ┴ └─┘
src ───┘ └────────────────────────────┘└─┘ └┘ └───────┘┴ └──┘ └─┘└─┘┴
typ ───┘ └────────────────────────────┘└─┘┴└┘ └───────┘┴┴└──┘ ┴ └─┘└─┘┴
doc ───┘ └─┘ └┘ └───────┘┴ └──┘ └─┘ ┴
txt ───┘ └─┘ └┘ ┴ └──┘ └─┘ ┴
par ───┘ └─┘ └┘ ┴ └──┘ └─┘ ┴
pid ───┘ └─┘ └┘ ┴ └──┘ └─┘ ┴
st ──────────────────────────────────────────────────────────────────┘└─
98 rw ← HN at HM,
id └┘
src └───┘ └────┘
typ └───┘└┘└────┘
doc └───┘ └────┘
txt └───┘ └────┘
par └───┘ └────┘
pid └─┘ └────┘
st ──────────────┘└─
99 have HN2 : D (N+1) ≤ D N := classical.by_contradiction (λ H, HM
id ┴ ┴ ┴ └────────────────────────┘ └┘
src └─────────┘ ┴ └─┘┴┴ ┴ └──┘└────────────────────────┘┴ └──┘ └
typ └─────────┘ ┴ └─┘┴┴┴┴┴└──┘└────────────────────────┘┴ └──┘└┘└
doc └─────────┘ ┴ └─┘ ┴ ┴ └──┘ ┴ └──┘ └
txt └─────────┘ ┴ └─┘ ┴ ┴ └──┘ ┴ └──┘ └
par └─────────┘ ┴ └─┘ ┴ ┴ └──┘ ┴ └──┘ └
pid └──────┘└─┘ ┴ └─┘ ┴ ┴ └──┘ ┴ └──┘ └
st ──────────────────────────────────────────────────────────────────
100 (lt_of_le_not_le (map_mono (degree_le_mono
id └─────────────┘ └──────┘ └────────────┘
src ───┘ └─────────────┘┴ └──────┘┴ └────────────┘└
typ ───┘ └─────────────┘┴ └──────┘┴ └────────────┘└
doc ───┘ ┴ ┴ └
txt ───┘ ┴ ┴ └
par ───┘ ┴ ┴ └
pid ───┘ ┴ ┴ └
st ───────────────────────────────────────────────
101 (with_bot.coe_le_coe.2 (nat.le_succ N)))) H)),
id └─────────────────┘ └─────────┘ ┴
src ─────┘ └─────────────────┘└─┘ └─────────┘┴ └───┘ └┘
typ ─────┘ └─────────────────┘└─┘ └─────────┘┴┴└───┘ └┘
doc ─────┘ └─┘ ┴ └───┘ └┘
txt ─────┘ └─┘ ┴ └───┘ └┘
par ─────┘ └─┘ ┴ └───┘ └┘
pid ─────┘ └─┘ ┴ └───┘ └┘
st ──────────────────────────────────────────────────┘└─
102 have HN3 : leval (X^(N+1)) ∈ D N,
id └───┘ ┴┴ ┴ ┴
src └─────────┘ ┴ ┴┴ └──┘ ┴ ┴
typ └─────────┘└───┘┴ ┴┴ └──┘ ┴┴┴┴
doc └─────────┘ ┴ ┴ └──┘ ┴ ┴
txt └─────────┘ ┴ └──┘ ┴ ┴
par └─────────┘ ┴ └──┘ ┴ ┴
pid └──────┘└─┘ ┴ └──┘ ┴ ┴
st ─────────────────────────────────┘└─
103 { exact HN2 (mem_map_of_mem (mem_degree_le.2 (degree_X_pow_le _))) },
id └─┘ └────────────┘ └───────────┘ └─────────────┘
src └────┘ ┴ └────────────┘┴ └───────────┘└─┘ └─────────────┘└────┘
typ └────┘└─┘┴ └────────────┘┴ └───────────┘└─┘ └─────────────┘└────┘
doc └────┘ ┴ ┴ └─┘ └────┘
txt └────┘ ┴ ┴ └─┘ └────┘
par └────┘ ┴ ┴ └─┘ └────┘
pid ┴ ┴ ┴ └─┘ └───┘┴
st ───┘└───────────────────────────────────────────────────────────────┘└┘└
104 rcases HN3 with ⟨p, hdp, hpe⟩,
id └─┘
src └─────┘ └─────────────────┘
typ └─────┘└─┘└─────────────────┘
doc └─────┘ └─────────────────┘
txt └─────┘ └─────────────────┘
par └─────┘ └─────────────────┘
pid ┴ └─────────────────┘
st ──────────────────────────────┘┴└
105 refine ⟨X^(N+1) - p, monic_X_pow_sub (mem_degree_le.1 hdp), _⟩,
id ┴ ┴ ┴ ┴ └─────────────┘ └───────────┘ └─┘
src └─────┘ ┴ └─┘┴┴ └┘└─────────────┘┴ └───────────┘└─┘ └───┘
typ └─────┘ ┴ ┴ └─┘┴┴┴└┘└─────────────┘┴ └───────────┘└─┘└─┘└───┘
doc └─────┘ ┴ └─┘ ┴ └┘ ┴ └─┘ └───┘
txt └─────┘ └─┘ ┴ └┘ ┴ └─┘ └───┘
par └─────┘ └─┘ ┴ └┘ ┴ └─┘ └───┘
pid ┴ └─┘ ┴ └┘ ┴ └─┘ └───┘
st ───────────────────────────────────────────────────────────────┘└─
106 show leval (X ^ (N + 1) - p) = 0,
id └───┘ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴┴ ┴ ┴ └──┘ ┴ └┘┴└┘
typ └───┘└───┘┴ ┴┴ ┴ ┴┴ └──┘ ┴┴└┘┴└┘
doc └───┘ ┴ ┴┴ ┴ ┴ └──┘ ┴ └┘ └┘
txt └───┘ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ └┘
par └───┘ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ └┘
pid └───┘ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ ┴┴
st ─────────────────────────────────┘└─
107 rw [linear_map.map_sub, hpe, sub_self]
id └────────────────┘ └─┘ └──────┘
src └──┘└────────────────┘└┘ └┘└──────┘└┘
typ └──┘└────────────────┘└┘└─┘└┘└──────┘└┘
doc └──┘ └┘ └┘ └┘
txt └──┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘
pid └┘ └┘ └┘ ┴┴
st ───────────────────────┘└───┘└────────┘┴┴
108 end
st └─┘
109
110 theorem is_integral_of_noetherian (S : subalgebra R A)
id └────────┘ ┴ ┴
src └────────┘
typ └────────┘ ┴ ┴
111 (H : is_noetherian R (S : submodule R A)) (x : A) (hx : x ∈ S) :
id └───────────┘ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────┘ └───────┘ ┴
typ └───────────┘ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────┘
112 is_integral R x :=
id └─────────┘ ┴ ┴
src └─────────┘
typ └─────────┘ ┴ ┴
113 begin
st └─────
114 letI : algebra R S := S.algebra,
id └─────┘ ┴ ┴ └───────┘
src └─────┘└─────┘┴ ┴ └──┘└───────┘
typ └─────┘└─────┘┴┴┴┴└──┘└───────┘
doc └─────┘└─────┘┴ ┴ └──┘
txt └─────┘ ┴ ┴ └──┘
par └─────┘ ┴ ┴ └──┘
pid ┴└┘ ┴ ┴ └──┘
st ────────────────────────────────┘└─
115 letI : comm_ring S := S.comm_ring R A,
id └───────┘ ┴ └─────────┘ ┴ ┴
src └─────┘└───────┘┴ └──┘└─────────┘┴ ┴
typ └─────┘└───────┘┴┴└──┘└─────────┘┴┴┴┴
doc └─────┘ ┴ └──┘ ┴ ┴
txt └─────┘ ┴ └──┘ ┴ ┴
par └─────┘ ┴ └──┘ ┴ ┴
pid ┴└┘ ┴ └──┘ ┴ ┴
st ──────────────────────────────────────┘└─
116 suffices : is_integral R (⟨x, hx⟩ : S),
id └─────────┘ ┴ ┴ └┘ ┴
src └─────────┘└─────────┘┴ ┴ └┘ └──┘ ┴
typ └─────────┘└─────────┘┴┴┴ ┴└┘└┘└──┘┴┴
doc └─────────┘ ┴ ┴ └┘ └──┘ ┴
txt └─────────┘ ┴ ┴ └┘ └──┘ ┴
par └─────────┘ ┴ ┴ └┘ └──┘ ┴
pid └───────┘└┘ ┴ ┴ └┘ └──┘ ┴
st ───────────────────────────────────────┘└─
117 { rcases this with ⟨p, hpm, hpx⟩,
id └──┘
src └─────┘ └─────────────────┘
typ └─────┘└──┘└─────────────────┘
doc └─────┘ └─────────────────┘
txt └─────┘ └─────────────────┘
par └─────┘ └─────────────────┘
pid ┴ └─────────────────┘
st ───┘└────────────────────────────┘└─
118 replace hpx := congr_arg subtype.val hpx,
id └───────┘ └─────────┘ └─┘
src └─────────────┘└───────┘┴└─────────┘┴
typ └─────────────┘└───────┘┴└─────────┘┴└─┘
doc └─────────────┘ ┴ ┴
txt └─────────────┘ ┴ ┴
par └─────────────┘ ┴ ┴
pid └──┘┴└─┘ ┴ ┴
st ───────────────────────────────────────────┘└─
119 refine ⟨p, hpm, eq.trans _ hpx⟩,
id ┴ └─┘ └──────┘ └─┘
src └─────┘ └┘ └┘└──────┘└─┘ ┴
typ └─────┘ ┴└┘└─┘└┘└──────┘└─┘└─┘┴
doc └─────┘ └┘ └┘ └─┘ ┴
txt └─────┘ └┘ └┘ └─┘ ┴
par └─────┘ └┘ └┘ └─┘ ┴
pid ┴ └┘ └┘ └─┘ ┴
st ──────────────────────────────────┘└─
120 simp only [aeval_def, eval₂, finsupp.sum],
id └───────┘ └───┘ └─────────┘
src └─────────┘└───────┘└┘└───┘└┘└─────────┘┴
typ └─────────┘└───────┘└┘└───┘└┘└─────────┘┴
doc └─────────┘ └┘└───┘└┘└─────────┘┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st ────────────────────────────────────────────┘└─
121 rw ← p.support.sum_hom subtype.val,
id └───────────────┘ └─────────┘
src └───┘└───────────────┘┴└─────────┘
typ └───┘└───────────────┘┴└─────────┘
doc └───┘ ┴
txt └───┘ ┴
par └───┘ ┴
pid └─┘ ┴
st ─────────────────────────────────────┘└─
122 { refine finset.sum_congr rfl (λ n hn, _),
id └──────────────┘ └─┘
src └─────┘└──────────────┘┴└─┘┴ └───────┘
typ └─────┘└──────────────┘┴└─┘┴ └───────┘
doc └─────┘ ┴ ┴ └───────┘
txt └─────┘ ┴ ┴ └───────┘
par └─────┘ ┴ ┴ └───────┘
pid ┴ ┴ ┴ └───────┘
st ─────┘└─────────────────────────────────────┘└─
123 change _ = _ * _,
id ┴ ┴
src └───────┘┴└─┘┴└┘
typ └───────┘┴└─┘┴└┘
doc └───────┘ └─┘ └┘
txt └───────┘ └─┘ └┘
par └───────┘ └─┘ └┘
pid └─┘ └─┘ └┘
st ─────────────────────┘└─
124 rw is_semiring_hom.map_pow subtype.val, refl,
id └─────────────────────┘ └─────────┘
src └─┘└─────────────────────┘┴└─────────┘ └──┘
typ └─┘└─────────────────────┘┴└─────────┘ └──┘
doc └─┘ ┴ └──┘
txt └─┘ ┴ └──┘
par └─┘ ┴ └──┘
pid ┴ ┴
st ───────────────────────────────────────────┘└────┘└─
125 split; intros; refl },
src └───┘ └────┘ └───┘
typ └───┘ └────┘ └───┘
doc └───┘ └────┘ └───┘
txt └───┘ └────┘ └───┘
par └───┘ └────┘ └───┘
pid ┴
st ─────────────────────────┘└┘└
126 refine { map_add := _, map_zero := _ }; intros; refl },
src └─────┘ └────────────────────────────┘ └────┘ └───┘
typ └─────┘ └────────────────────────────┘ └────┘ └───┘
doc └─────┘ └────────────────────────────┘ └────┘ └───┘
txt └─────┘ └────────────────────────────┘ └────┘ └───┘
par └─────┘ └────────────────────────────┘ └────┘ └───┘
pid ┴ └────────────────────────────┘ ┴
st ────────────────────────────────────────────────────────┘└┘└
127 refine is_integral_of_noetherian' H ⟨x, hx⟩
id └────────────────────────┘ ┴ ┴ └┘
src └─────┘└────────────────────────┘┴ ┴ └┘ └┘
typ └─────┘└────────────────────────┘┴┴┴ ┴└┘└┘└┘
doc └─────┘ ┴ ┴ └┘ └┘
txt └─────┘ ┴ ┴ └┘ └┘
par └─────┘ ┴ ┴ └┘ └┘
pid ┴ ┴ ┴ └┘ ┴┴
st ─────────────────────────────────────────────┘
128 end
st └─┘
129
130 set_option class.instance_max_depth 100
doc └──────────────────────┘
131 theorem is_integral_of_mem_of_fg (S : subalgebra R A)
id └────────┘ ┴ ┴
src └────────┘
typ └────────┘ ┴ ┴
132 (HS : (S : submodule R A).fg) (x : A) (hx : x ∈ S) : is_integral R x :=
id ┴ └───────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴
src └───────┘ └┘ ┴ └─────────┘
typ ┴ └───────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴
doc └───────┘
133 begin
st └─────
134 cases HS with y hy,
id └┘
src └────┘ └────────┘
typ └────┘└┘└────────┘
doc └────┘ └────────┘
txt └────┘ └────────┘
par └────┘ └────────┘
pid ┴ └────────┘
st ───────────────────┘└─
135 obtain ⟨lx, hlx1, hlx2⟩ :
src └─────────────────────────
typ └─────────────────────────
doc └─────────────────────────
txt └─────────────────────────
par └─────────────────────────
pid └───────────────────
st ────────────────────────────
136 ∃ (l : A →₀ R) (H : l ∈ finsupp.supported R R ↑y), (finsupp.total A A R id) l = x,
id ┴ └┘ ┴ └───────────────┘ ┴┴ ┴ └───────────┘ ┴ ┴ └┘ ┴ ┴
src ───┘┴└────┘ ┴└┘┴ └─────┘ ┴┴┴└───────────────┘┴ ┴ ┴┴ ┴┴┴ └───────────┘┴ ┴ ┴ ┴└┘└┘ ┴┴┴
typ ───┘┴└────┘ ┴└┘┴ └─────┘ ┴┴┴└───────────────┘┴ ┴ ┴┴┴┴┴┴ └───────────┘┴ ┴┴┴┴┴└┘└┘ ┴┴┴┴
doc ───┘ └────┘ ┴└┘┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘┴ ┴ ┴ ┴ └┘ ┴ ┴
txt ───┘ └────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
par ───┘ └────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
pid ───┘ └────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
st ────────────────────────────────────────────────────────────────────────────────────┘└─
137 { rwa [←(@finsupp.mem_span_iff_total A A R _ _ _ id ↑y x), set.image_id ↑y, hy] },
id └────────────────────────┘ ┴ ┴ └┘ ┴ ┴ └──────────┘ ┴ └┘
src └────┘ └────────────────────────┘┴ ┴ ┴ └─────┘└┘┴ ┴ └─┘└──────────┘┴ └┘ └┘
typ └────┘ └────────────────────────┘┴ ┴┴┴┴└─────┘└┘┴ ┴┴┴└─┘└──────────┘┴ ┴└┘└┘└┘
doc └────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ └─┘ ┴ └┘ └┘
txt └────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ └─┘ ┴ └┘ └┘
par └────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ └─┘ ┴ └┘ └┘
pid └─┘ ┴ ┴ ┴ └─────┘ ┴ ┴ └─┘ ┴ └┘ ┴┴
st ───┘└─────────────────────────────────────────────────────┘└───────────────┘└──┘┴┴└┘└
138 have : ∀ (jk : (↑(y.product y) : set (A × A))), jk.1.1 * jk.1.2 ∈ (span R ↑y : submodule R A),
id ┴ └───────┘ └─┘ ┴ ┴ └──┘ ┴ ┴ └───────┘ ┴
src └─────┘ └─────┘ └───────┘┴ └──┘└─┘┴ ┴┴┴ └─┘ ┴ └───┘┴┴ └───┘ ┴ └──┘┴ ┴ └─┘└───────┘┴ ┴ ┴
typ └─────┘ └─────┘┴ └───────┘┴ └──┘└─┘┴ ┴┴┴ └─┘ ┴ └───┘┴┴ └───┘ ┴ └──┘┴┴┴ ┴└─┘└───────┘┴ ┴┴┴
doc └─────┘ └─────┘ └───────┘┴ └──┘ ┴ ┴ ┴ └─┘ ┴ └───┘ ┴ └───┘ ┴ └──┘┴ ┴ └─┘└───────┘┴ ┴ ┴
txt └─────┘ └─────┘ ┴ └──┘ ┴ ┴ ┴ └─┘ ┴ └───┘ ┴ └───┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
par └─────┘ └─────┘ ┴ └──┘ ┴ ┴ ┴ └─┘ ┴ └───┘ ┴ └───┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
pid └───┘└┘ └─────┘ ┴ └──┘ ┴ ┴ ┴ └─┘ ┴ └───┘ ┴ └───┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
139 { intros jk,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
pid └─┘
st ───┘└───────┘└─
140 let j : ↥(↑y : set A) := ⟨jk.1.1, (finset.mem_product.1 jk.2).1⟩,
id ┴ ┴ └─┘ ┴ └────────────────┘ └┘
src └──────┘┴ └─┘└─┘┴ └───┘ └────┘ └────────────────┘└─┘ └────┘
typ └──────┘┴ ┴└─┘└─┘┴┴└───┘ └────┘ └────────────────┘└─┘└┘└────┘
doc └──────┘ └─┘ ┴ └───┘ └────┘ └─┘ └────┘
txt └──────┘ └─┘ ┴ └───┘ └────┘ └─┘ └────┘
par └──────┘ └─┘ ┴ └───┘ └────┘ └─┘ └────┘
pid └───┘└─┘ └─┘ ┴ ┴└──┘ └────┘ └─┘ └────┘
st ───────────────────────────────────────────────────────────────────┘└─
141 let k : ↥(↑y : set A) := ⟨jk.1.2, (finset.mem_product.1 jk.2).2⟩,
id ┴ └─┘ ┴ └────────────────┘ └┘
src └──────┘ └─┘└─┘┴ └───┘ └────┘ └────────────────┘└─┘ └────┘
typ └──────┘ ┴└─┘└─┘┴┴└───┘ └────┘ └────────────────┘└─┘└┘└────┘
doc └──────┘ └─┘ ┴ └───┘ └────┘ └─┘ └────┘
txt └──────┘ └─┘ ┴ └───┘ └────┘ └─┘ └────┘
par └──────┘ └─┘ ┴ └───┘ └────┘ └─┘ └────┘
pid └───┘└─┘ └─┘ ┴ ┴└──┘ └────┘ └─┘ └────┘
st ───────────────────────────────────────────────────────────────────┘└─
142 have hj : j.1 ∈ (span R ↑y : submodule R A) := subset_span j.2,
id ┴ └──┘ ┴ ┴ └───────┘ ┴ └─────────┘ ┴
src └────────┘ └─┘ ┴ └──┘┴ ┴ └─┘└───────┘┴ ┴ └───┘└─────────┘┴ └┘
typ └────────┘┴└─┘ ┴ └──┘┴┴┴ ┴└─┘└───────┘┴ ┴┴└───┘└─────────┘┴┴└┘
doc └────────┘ └─┘ ┴ └──┘┴ ┴ └─┘└───────┘┴ ┴ └───┘ ┴ └┘
txt └────────┘ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └───┘ ┴ └┘
par └────────┘ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └───┘ ┴ └┘
pid └─────┘└─┘ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴└──┘ ┴ └┘
st ─────────────────────────────────────────────────────────────────┘└─
143 have hk : k.1 ∈ (span R ↑y : submodule R A) := subset_span k.2,
id ┴ └──┘ ┴ ┴ └───────┘ ┴ └─────────┘ ┴
src └────────┘ └─┘ ┴ └──┘┴ ┴ └─┘└───────┘┴ ┴ └───┘└─────────┘┴ └┘
typ └────────┘┴└─┘ ┴ └──┘┴┴┴ ┴└─┘└───────┘┴ ┴┴└───┘└─────────┘┴┴└┘
doc └────────┘ └─┘ ┴ └──┘┴ ┴ └─┘└───────┘┴ ┴ └───┘ ┴ └┘
txt └────────┘ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └───┘ ┴ └┘
par └────────┘ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └───┘ ┴ └┘
pid └─────┘└─┘ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴└──┘ ┴ └┘
st ─────────────────────────────────────────────────────────────────┘└─
144 revert hj hk, rw hy, exact @is_submonoid.mul_mem A _ S _ j.1 k.1 },
id └┘ └──────────────────┘ ┴ ┴ ┴ ┴
src └──────────┘ └─┘ └────┘ └──────────────────┘┴ └─┘ └─┘ └─┘ └─┘
typ └──────────┘ └─┘└┘ └────┘ └──────────────────┘┴┴└─┘┴└─┘┴└─┘┴└─┘
doc └──────────┘ └─┘ └────┘ ┴ └─┘ └─┘ └─┘ └─┘
txt └──────────┘ └─┘ └────┘ ┴ └─┘ └─┘ └─┘ └─┘
par └──────────┘ └─┘ └────┘ ┴ └─┘ └─┘ └─┘ └─┘
pid └────┘ ┴ ┴ ┴ └─┘ └─┘ └─┘ └─┘
st ───────────────┘└─────┘└────────────────────────────────────────────┘└┘└
145 rw ← set.image_id ↑y at this,
id └──────────┘ ┴
src └───┘└──────────┘┴ └──────┘
typ └───┘└──────────┘┴ ┴└──────┘
doc └───┘ ┴ └──────┘
txt └───┘ ┴ └──────┘
par └───┘ ┴ └──────┘
pid └─┘ ┴ └──────┘
st ─────────────────────────────┘└─
146 simp only [finsupp.mem_span_iff_total] at this,
id └────────────────────────┘
src └─────────┘└────────────────────────┘└───────┘
typ └─────────┘└────────────────────────┘└───────┘
doc └─────────┘ └───────┘
txt └─────────┘ └───────┘
par └─────────┘ └───────┘
pid ┴└──┘└┘ ┴┴└─────┘
st ───────────────────────────────────────────────┘└─
147 choose ly hly1 hly2,
src └─────────────────┘
typ └─────────────────┘
doc └─────────────────┘
txt └─────────────────┘
par └─────────────────┘
pid └─┘└────────┘
st ────────────────────┘└─
148 let S₀' : finset R := lx.frange ∪ finset.bind finset.univ (finsupp.frange ∘ ly),
id └────┘ ┴ └───────┘ ┴ └─────────┘ └─────────┘ └────────────┘ ┴ └┘
src └────────┘└────┘┴ └──┘└───────┘┴┴┴└─────────┘┴└─────────┘┴ └────────────┘┴┴┴ ┴
typ └────────┘└────┘┴┴└──┘└───────┘┴┴┴└─────────┘┴└─────────┘┴ └────────────┘┴┴┴└┘┴
doc └────────┘└────┘┴ └──┘ ┴ ┴└─────────┘┴└─────────┘┴ ┴ ┴ ┴
txt └────────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └────────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └─────┘└─┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────────────────────────┘└─
149 let S₀ : set R := ring.closure ↑S₀',
id └─┘ ┴ └──────────┘ └─┘
src └───────┘└─┘┴ └──┘└──────────┘┴
typ └───────┘└─┘┴┴└──┘└──────────┘┴ └─┘
doc └───────┘ ┴ └──┘ ┴
txt └───────┘ ┴ └──┘ ┴
par └───────┘ ┴ └──┘ ┴
pid └────┘└─┘ ┴ └──┘ ┴
st ────────────────────────────────────┘└─
150 refine is_integral_of_subring (ring.closure ↑S₀') _,
id └────────────────────┘ └──────────┘ └─┘
src └─────┘└────────────────────┘┴ └──────────┘┴ └─┘
typ └─────┘└────────────────────┘┴ └──────────┘┴ └─┘└─┘
doc └─────┘ ┴ ┴ └─┘
txt └─────┘ ┴ ┴ └─┘
par └─────┘ ┴ ┴ └─┘
pid ┴ ┴ ┴ └─┘
st ────────────────────────────────────────────────────┘└─
151 letI : algebra S₀ (algebra.comap S₀ R A) := algebra.comap.algebra _ _ _,
id └─────┘ └───────────┘ └┘ ┴ ┴ └───────────────────┘
src └─────┘└─────┘┴ ┴ └───────────┘┴ ┴ ┴ └───┘└───────────────────┘└────┘
typ └─────┘└─────┘┴ ┴ └───────────┘┴└┘┴┴┴┴└───┘└───────────────────┘└────┘
doc └─────┘└─────┘┴ ┴ └───────────┘┴ ┴ ┴ └───┘└───────────────────┘└────┘
txt └─────┘ ┴ ┴ ┴ ┴ ┴ └───┘ └────┘
par └─────┘ ┴ ┴ ┴ ┴ ┴ └───┘ └────┘
pid ┴└┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ └────┘
st ────────────────────────────────────────────────────────────────────────┘└─
152 letI hmod : module S₀ (algebra.comap S₀ R A) := algebra.to_module,
id └────┘ └───────────┘ └┘ ┴ ┴ └───────────────┘
src └──────────┘└────┘┴ ┴ └───────────┘┴ ┴ ┴ └───┘└───────────────┘
typ └──────────┘└────┘┴ ┴ └───────────┘┴└┘┴┴┴┴└───┘└───────────────┘
doc └──────────┘└────┘┴ ┴ └───────────┘┴ ┴ ┴ └───┘
txt └──────────┘ ┴ ┴ ┴ ┴ ┴ └───┘
par └──────────┘ ┴ ┴ ┴ ┴ ┴ └───┘
pid └───┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘
st ──────────────────────────────────────────────────────────────────┘└─
153 have : (span S₀ (insert 1 (↑y:set A) : set (algebra.comap S₀ R A)) : submodule S₀ (algebra.comap S₀ R A)) =
id └──┘ └────┘ └───────┘
src └─────┘ └──┘┴ ┴ └────┘└─┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └───┘└───────┘┴ ┴ ┴ ┴ ┴ └─┘ └
typ └─────┘ └──┘┴ ┴ └────┘└─┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └───┘└───────┘┴ ┴ ┴ ┴ ┴ └─┘ └
doc └─────┘ └──┘┴ ┴ └─┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └───┘└───────┘┴ ┴ ┴ ┴ ┴ └─┘ └
txt └─────┘ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └─┘ └
par └─────┘ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └─┘ └
pid └───┘└┘ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └─┘ └
st ──────────────────────────────────────────────────────────────────────────────────────────────────────────────
154 (algebra.adjoin S₀ ((↑y : set A) : set (algebra.comap S₀ R A)) : subalgebra S₀ (algebra.comap S₀ R A)),
id └────────────┘ ┴ └─┘ ┴ └───────────┘ └┘ ┴ └────────┘
src ─────┘ └────────────┘┴ ┴ └─┘└─┘┴ └──┘ ┴ └───────────┘┴ ┴ ┴ └───┘└────────┘┴ ┴ ┴ ┴ ┴ └┘
typ ─────┘ └────────────┘┴ ┴ ┴└─┘└─┘┴┴└──┘ ┴ └───────────┘┴└┘┴┴┴ └───┘└────────┘┴ ┴ ┴ ┴ ┴ └┘
doc ─────┘ ┴ ┴ └─┘ ┴ └──┘ ┴ └───────────┘┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └┘
txt ─────┘ ┴ ┴ └─┘ ┴ └──┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └┘
par ─────┘ ┴ ┴ └─┘ ┴ └──┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └┘
pid ─────┘ ┴ ┴ └─┘ ┴ └──┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └┘
st ───────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
155 { apply le_antisymm,
id └─────────┘
src └────┘└─────────┘
typ └────┘└─────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───┘└───────────────┘└─
156 { rw [span_le, set.insert_subset, mem_coe], split,
id └─────┘ └───────────────┘
src └──┘└─────┘└┘└───────────────┘
typ └──┘└─────┘└┘└───────────────┘
doc └──┘ └┘
txt └──┘ └┘
par └──┘ └┘
pid └┘ └┘
st ─────┘└─────────┘└─────────────────┘
157 change _ ∈ ring.closure _, exact is_submonoid.one_mem _, exact algebra.subset_adjoin },
st └┘
158 rw [algebra.adjoin_eq_span, span_le], intros r hr, refine monoid.in_closure.rec_on hr _ _ _,
159 { intros r hr, exact subset_span (set.mem_insert_of_mem _ hr) },
st └┘
160 { exact subset_span (set.mem_insert _ _) },
st └┘
161 intros r1 r2 hr1 hr2 ih1 ih2,
162 rw ← set.image_id (insert _ ↑y) at ih1 ih2,
id ┴
typ ┴
163 simp only [mem_coe, finsupp.mem_span_iff_total] at ih1 ih2,
164 have ih1' := ih1, have ih2' := ih2,
165 rcases ih1' with ⟨l1, hl1, rfl⟩, rcases ih2' with ⟨l2, hl2, rfl⟩,
166 simp only [finsupp.total_apply, finsupp.sum_mul, finsupp.mul_sum, mem_coe],
167 rw [finsupp.sum], refine sum_mem _ _, intros r2 hr2,
168 rw [finsupp.sum], refine sum_mem _ _, intros r1 hr1,
169 rw [algebra.mul_smul_comm, algebra.smul_mul_assoc],
170 letI : module ↥S₀ A := hmod, refine smul_mem _ _ (smul_mem _ _ _),
id └┘ ┴
typ └┘ ┴
171 rcases hl1 hr1 with rfl | hr1,
172 { change 1 * r2 ∈ _, rw one_mul r2, exact subset_span (hl2 hr2) },
st └┘
173 rcases hl2 hr2 with rfl | hr2,
174 { change r1 * 1 ∈ _, rw mul_one, exact subset_span (set.mem_insert_of_mem _ hr1) },
st └┘
175 let jk : ↥(↑(finset.product y y) : set (A × A)) := ⟨(r1, r2), finset.mem_product.2 ⟨hr1, hr2⟩⟩,
id ┴ └─┘ ┴
src └─┘
typ ┴ └─┘ ┴
176 specialize hly2 jk, change _ = r1 * r2 at hly2, rw [id, id, ← hly2, finsupp.total_apply],
177 rw [finsupp.sum], refine sum_mem _ _, intros z hz,
178 have : ly jk z ∈ S₀,
id ┴ └┘
typ ┴ └┘
179 { apply ring.subset_closure,
180 apply finset.mem_union_right, apply finset.mem_bind.2,
181 exact ⟨jk, finset.mem_univ _, by convert finset.mem_image_of_mem _ hz⟩ },
st └┘
182 change @has_scalar.smul S₀ (algebra.comap S₀ R A) hmod.to_has_scalar ⟨ly jk z, this⟩ z ∈ _,
id └┘ ┴ ┴ ┴
typ └┘ ┴ ┴ ┴
183 exact smul_mem _ _ (subset_span (set.mem_insert_of_mem _ (hly1 _ hz))) },
st └┘
184 haveI : is_noetherian_ring ↥S₀ :=
id └┘
typ └┘
185 by { convert is_noetherian_ring_closure _ (finset.finite_to_set _), apply_instance },
st └┘
186 apply is_integral_of_noetherian
187 (algebra.adjoin S₀ ((↑y : set A) : set (algebra.comap S₀ R A)) : subalgebra S₀ (algebra.comap S₀ R A))
id └─┘ ┴ ┴
src └─┘
typ └─┘ ┴ ┴
188 (is_noetherian_of_fg_of_noetherian _ ⟨insert 1 y, by rw finset.coe_insert; convert this⟩),
id ┴
typ ┴
189 show x ∈ ((algebra.adjoin S₀ ((↑y : set A) : set (algebra.comap S₀ R A)) :
id ┴ ┴ └─┘ ┴ ┴
src └─┘
typ ┴ ┴ └─┘ ┴ ┴
190 subalgebra S₀ (algebra.comap S₀ R A)) : submodule S₀ (algebra.comap S₀ R A)),
191 rw [← hlx2, finsupp.total_apply, finsupp.sum], refine sum_mem _ _, intros r hr,
192 rw ← this,
193 have : lx r ∈ ring.closure ↑S₀' :=
id ┴ └─┘
typ ┴ └─┘
194 ring.subset_closure (finset.mem_union_left _ (by convert finset.mem_image_of_mem _ hr)),
195 change @has_scalar.smul S₀ (algebra.comap S₀ R A) hmod.to_has_scalar ⟨lx r, this⟩ r ∈ _,
id └┘ ┴ ┴ ┴
typ └┘ ┴ ┴ ┴
196 rw finsupp.mem_supported at hlx1,
197 exact smul_mem _ _ (subset_span (set.mem_insert_of_mem _ (hlx1 hr))),
198 end
st └─┘
199
200 theorem is_integral_of_mem_closure {x y z : A}
id ┴
typ ┴
201 (hx : is_integral R x) (hy : is_integral R y)
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
202 (hz : z ∈ ring.closure ({x, y} : set A)) :
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
203 is_integral R z :=
id ┴ ┴
typ ┴ ┴
204 begin
205 have := fg_mul _ _ (fg_adjoin_singleton_of_integral x hx) (fg_adjoin_singleton_of_integral y hy),
id ┴ ┴
typ ┴ ┴
206 rw [← algebra.adjoin_union_coe_submodule, set.union_singleton, insert] at this,
207 exact is_integral_of_mem_of_fg (algebra.adjoin R {x, y}) this z
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
208 (ring.closure_mono (set.subset_union_right _ _) hz)
209 end
st └─┘
210
211 theorem is_integral_zero : is_integral R (0:A) :=
id ┴ ┴
typ ┴ ┴
212 algebra.map_zero R A ▸ is_integral_algebra_map
id ┴ ┴
typ ┴ ┴
213
214 theorem is_integral_one : is_integral R (1:A) :=
id ┴ ┴
typ ┴ ┴
215 algebra.map_one R A ▸ is_integral_algebra_map
id ┴ ┴
typ ┴ ┴
216
217 theorem is_integral_add {x y : A}
id ┴
typ ┴
218 (hx : is_integral R x) (hy : is_integral R y) :
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
219 is_integral R (x + y) :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
220 is_integral_of_mem_closure hx hy (is_add_submonoid.add_mem
221 (ring.subset_closure (or.inr (or.inl rfl))) (ring.subset_closure (or.inl rfl)))
222
223 theorem is_integral_neg {x : A}
id ┴
typ ┴
224 (hx : is_integral R x) : is_integral R (-x) :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
225 is_integral_of_mem_closure hx hx (is_add_subgroup.neg_mem
226 (ring.subset_closure (or.inl rfl)))
227
228 theorem is_integral_sub {x y : A}
id ┴
typ ┴
229 (hx : is_integral R x) (hy : is_integral R y) : is_integral R (x - y) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
230 is_integral_add hx (is_integral_neg hy)
231
232 theorem is_integral_mul {x y : A}
233 (hx : is_integral R x) (hy : is_integral R y) :
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
234 is_integral R (x * y) :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
235 is_integral_of_mem_closure hx hy (is_submonoid.mul_mem
236 (ring.subset_closure (or.inr (or.inl rfl))) (ring.subset_closure (or.inl rfl)))
237
238 variables (R A)
239 def integral_closure : subalgebra R A :=
id ┴ ┴
typ ┴ ┴
240 { carrier := { r | is_integral R r },
id ┴ ┴ ┴
typ ┴ ┴ ┴
241 subring :=
242 { zero_mem := is_integral_zero,
243 one_mem := is_integral_one,
244 add_mem := λ _ _, is_integral_add,
id ┴ ┴
typ ┴ ┴
245 neg_mem := λ _, is_integral_neg,
id ┴
typ ┴
246 mul_mem := λ _ _, is_integral_mul },
id ┴ ┴
typ ┴ ┴
247 range_le' := λ y ⟨x, hx⟩, hx ▸ is_integral_algebra_map }
id ┴ ┴ └─────────────────────┘
src ┴ └─────────────────────┘
typ ┴ ┴ └─────────────────────┘
248
249 theorem mem_integral_closure_iff_mem_fg {r : A} :
id ┴
typ ┴
250 r ∈ integral_closure R A ↔ ∃ M : subalgebra R A, (M : submodule R A).fg ∧ r ∈ M :=
id ┴ ┴ └──────────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴┴ ┴ └───────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
src ┴ └──────────────┘ ┴ ┴ └────────┘ ┴ └───────┘ └┘ ┴ ┴
typ ┴ ┴ └──────────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴┴ ┴ └───────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
doc └───────┘
251 ⟨λ hr, ⟨algebra.adjoin R {r}, fg_adjoin_singleton_of_integral _ hr, algebra.subset_adjoin (or.inl rfl)⟩,
id └┘ └────────────┘ ┴ ┴┴ └─────────────────────────────┘ └┘ └───────────────────┘ └────┘ └─┘
src └────────────┘ ┴ └─────────────────────────────┘ └───────────────────┘ └────┘ └─┘
typ └┘ └────────────┘ ┴ ┴┴ └─────────────────────────────┘ └┘ └───────────────────┘ └────┘ └─┘
252 λ ⟨M, Hf, hrM⟩, is_integral_of_mem_of_fg M Hf _ hrM⟩
id ┴┴ └┘ └─┘ └──────────────────────┘
src └──────────────────────┘
typ ┴┴ └┘ └─┘ └──────────────────────┘
253
254 theorem integral_closure_idem : integral_closure (integral_closure R A : set A) A = ⊥ :=
id └──────────────┘ └──────────────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src └──────────────┘ └──────────────┘ └─┘ ┴ ┴
typ └──────────────┘ └──────────────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
255 begin
st └─────
256 rw lattice.eq_bot_iff, intros r hr,
id └────────────────┘
src └─┘└────────────────┘
typ └─┘└────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────────────────┘
257 rcases is_integral_iff_is_integral_closure_finite.1 hr with ⟨s, hfs, hr⟩,
258 apply algebra.mem_bot.2, refine ⟨⟨_, _⟩, rfl⟩,
259 refine (mem_integral_closure_iff_mem_fg _ _).2 ⟨algebra.adjoin _ (subtype.val '' s ∪ {r}),
id ┴
typ ┴
260 algebra.fg_trans
261 (fg_adjoin_of_finite (set.finite_image _ hfs)
262 (λ y ⟨x, hx, hxy⟩, hxy ▸ x.2))
id ┴
typ ┴
263 _,
264 algebra.subset_adjoin (or.inr (or.inl rfl))⟩,
265 refine fg_adjoin_singleton_of_integral _ _,
266 rcases hr with ⟨p, hmp, hpx⟩,
267 refine ⟨to_subring (of_subring _ (of_subring _ p)) _ _, _, hpx⟩,
268 { intros x hx, rcases finsupp.mem_frange.1 hx with ⟨h1, n, rfl⟩,
269 change (coeff p n).1.1 ∈ ring.closure _,
id ┴
typ ┴
270 rcases ring.exists_list_of_mem_closure (coeff p n).2 with ⟨L, HL1, HL2⟩, rw ← HL2,
id ┴
typ ┴
271 clear HL2 hfs h1 hx n hmp hpx hr r p,
272 induction L with hd tl ih, { exact is_add_submonoid.zero_mem _ },
st └┘
273 rw list.forall_mem_cons at HL1,
274 rw [list.map_cons, list.sum_cons],
275 refine is_add_submonoid.add_mem _ (ih HL1.2),
276 cases HL1 with HL HL', clear HL' ih tl,
277 induction hd with hd tl ih, { exact is_submonoid.one_mem _ },
st └┘
278 rw list.forall_mem_cons at HL,
279 rw list.prod_cons,
280 refine is_submonoid.mul_mem _ (ih HL.2),
281 rcases HL.1 with hs | rfl,
282 { exact algebra.subset_adjoin (set.mem_image_of_mem _ hs) },
st └┘
283 exact is_add_subgroup.neg_mem (is_submonoid.one_mem _) },
st └┘
284 replace hmp := congr_arg subtype.val hmp,
285 replace hmp := congr_arg subtype.val hmp,
286 exact subtype.eq hmp
287 end
st └─┘
288
289 end
290
291 section algebra
292 open algebra
293 variables {R : Type*} {A : Type*} {B : Type*}
294 variables [comm_ring R] [comm_ring A] [comm_ring B]
id └───────┘ └───────┘ └───────┘
src └───────┘ └───────┘ └───────┘
typ └───────┘ └───────┘ └───────┘
295 variables [algebra R A] [algebra A B]
id └─────┘ └─────┘
src └─────┘ └─────┘
typ └─────┘ └─────┘
doc └─────┘ └─────┘
296
297 set_option class.instance_max_depth 50
doc └──────────────────────┘
298
299 lemma is_integral_trans_aux (x : B) {p : polynomial A} (pmonic : monic p) (hp : aeval A B x p = 0)
id ┴ └────────┘ ┴ └───┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
src └────────┘ └───┘ └───┘ ┴
typ ┴ └────────┘ ┴ └───┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
doc └────────┘ └───┘ └───┘
300 (S : set (comap R A B))
id └─┘ └───┘ ┴ ┴ ┴
src └─┘ └───┘
typ └─┘ └───┘ ┴ ┴ ┴
doc └───┘
301 (hS : S = (↑((finset.range (p.nat_degree + 1)).image
id ┴ ┴ ┴ └──────────┘ ┴└─────────┘ ┴ └───┘
src ┴ ┴ └──────────┘ └─────────┘ ┴ └───┘
typ ┴ ┴ ┴ └──────────┘ ┴└─────────┘ ┴ └───┘
doc └──────────┘ └─────────┘ └───┘
302 (λ i, to_comap R A B (p.coeff i))) : set (comap R A B))) :
id ┴ └──────┘ ┴ ┴ ┴ ┴└────┘ ┴ └─┘ └───┘ ┴ ┴ ┴
src └──────┘ └────┘ └─┘ └───┘
typ ┴ └──────┘ ┴ ┴ ┴ ┴└────┘ ┴ └─┘ └───┘ ┴ ┴ ┴
doc └────┘ └───┘
303 is_integral (adjoin R S) (comap.to_comap R A B x) :=
id └─────────┘ └────┘ ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴
src └─────────┘ └────┘ └────────────┘
typ └─────────┘ └────┘ ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴
304 begin
st └─────
305 have coeffs_mem : ∀ i, coeff (map (to_comap R A B) p) i ∈ adjoin R S,
id └───┘ └─┘ └──────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴
src └────────────────┘ └┘ ┴└───┘┴ └─┘┴ └──────┘┴ ┴ ┴ └┘ └┘ ┴┴┴└────┘┴ ┴
typ └────────────────┘ └┘ ┴└───┘┴ └─┘┴ └──────┘┴ ┴┴┴┴└┘┴└┘ ┴┴┴└────┘┴┴┴┴
doc └────────────────┘ └┘ ┴└───┘┴ └─┘┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴
txt └────────────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴
par └────────────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴
pid └─────────────┘└─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────┘
306 { intro i,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st └─────┘└─
307 by_cases hi : i ∈ finset.range (p.nat_degree + 1),
id ┴ └──────────┘ └──────────┘ ┴
src └───────┘ └─┘ ┴ ┴└──────────┘┴ └──────────┘┴┴└─┘
typ └───────┘ └─┘┴┴ ┴└──────────┘┴ └──────────┘┴┴└─┘
doc └───────┘ └─┘ ┴ ┴└──────────┘┴ └──────────┘┴ └─┘
txt └───────┘ └─┘ ┴ ┴ ┴ ┴ └─┘
par └───────┘ └─┘ ┴ ┴ ┴ ┴ └─┘
pid ┴ └─┘ ┴ ┴ ┴ ┴ └─┘
st ────────────────────────────────────────────────────┘
308 { apply algebra.subset_adjoin, subst S,
309 rw [finset.mem_coe, finset.mem_image, coeff_map],
310 exact ⟨i, hi, rfl⟩ },
id ┴
typ ┴
st └┘
311 { rw [finset.mem_range, not_lt] at hi,
312 rw [coeff_map, coeff_eq_zero_of_nat_degree_lt hi, alg_hom.map_zero],
313 exact submodule.zero_mem (adjoin R S : submodule R (comap R A B)) } },
id ┴ ┴ ┴
typ ┴ ┴ ┴
st └──┘
314 obtain ⟨q, hq⟩ : ∃ q : polynomial (adjoin R S), q.map (algebra_map (comap R A B)) =
315 (p.map $ to_comap R A B),
id ┴ ┴ ┴
typ ┴ ┴ ┴
316 { rw [← set.mem_range], dsimp only,
317 apply (polynomial.mem_map_range _).2,
318 { intros i, specialize coeffs_mem i, rw ← subalgebra.mem_coe at coeffs_mem,
id ┴
typ ┴
319 convert coeffs_mem, exact subtype.val_range },
st └┘
320 { apply is_ring_hom.is_semiring_hom } },
st └──┘
321 use q,
322 split,
323 { suffices h : (q.map (algebra_map (comap R A B))).monic,
id ┴ ┴ ┴
typ ┴ ┴ ┴
324 { refine @monic_of_injective _ _ _ _ _
325 (by exact is_ring_hom.is_semiring_hom _) _ _ h,
326 exact subtype.val_injective },
st └┘
327 { rw hq, exact monic_map _ pmonic } },
id └┘
typ └┘
st └──┘
328 { convert hp using 1,
329 replace hq := congr_arg (eval (comap.to_comap R A B x)) hq,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴
doc ┴ ┴
330 convert hq using 1; symmetry, swap,
id └──────┘
src └──────┘
typ └──────┘
doc └──────┘
331 exact eval_map _ _,
id └──────┘
src └──────┘
typ └──────┘
332 refine @eval_map _ _ _ _ _ _ (by exact is_ring_hom.is_semiring_hom _) _ },
id └──────┘ └─────────────────────────┘
src └──────┘ └─────────────────────────┘
typ └──────┘ └─────────────────────────┘
doc └─────────────────────────┘
st └┘
333 end
st └─┘
334
335 /-- If A is an R-algebra all of whose elements are integral over R,
336 and x is an element of an A-algebra that is integral over A, then x is integral over R.-/
337 lemma is_integral_trans (A_int : ∀ x : A, is_integral R x) (x : B) (hx : is_integral A x) :
id ┴ └─────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴
src └─────────┘ └─────────┘
typ ┴ └─────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴
338 is_integral R (comap.to_comap R A B x) :=
id └─────────┘ ┴ └────────────┘ ┴ ┴ ┴ ┴
src └─────────┘ └────────────┘
typ └─────────┘ ┴ └────────────┘ ┴ ┴ ┴ ┴
339 begin
st └─────
340 rcases hx with ⟨p, pmonic, hp⟩,
id └┘
src └─────┘ └───────────────────┘
typ └─────┘└┘└───────────────────┘
doc └─────┘ └───────────────────┘
txt └─────┘ └───────────────────┘
par └─────┘ └───────────────────┘
pid ┴ └───────────────────┘
st ───────────────────────────────┘┴
341 let S : set (comap R A B) :=
id └─┘ └───┘ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ └─┘ └───┘┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ └─┘ └───┘┴┴┴┴┴┴┴ ┴ ┴
doc ┴ ┴ ┴ ┴ └───┘┴ ┴ ┴ ┴ ┴ ┴
txt ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st └─┘ ┴ ┴ ┴ └─┘ └───────────┘ ┴ ┴
342 (↑((finset.range (p.nat_degree + 1)).image
id ┴ └──────────┘ └──────────┘ ┴
src ┴ ┴ ┴ └──────────┘ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ └──────────┘ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴ └──────────┘ └──────────┘ ┴ ┴ ┴ ┴ ┴
txt ┴ ┴ ┴ ┴ ┴ ┴ ┴
par ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴
343 (λ i, to_comap R A B (p.coeff i))) : set (comap R A B)),
id └──────┘ ┴ ┴ ┴ └─────┘ └─┘ └───┘
src ┴ ┴ ┴ ┴ ┴ └──────┘┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴└─┘┴ └───┘ ┴
typ ┴ ┴ ┴ ┴ ┴ └──────┘┴┴┴┴┴┴┴ └─────┘ ┴ ┴ ┴└─┘┴ └───┘ ┴
doc ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ └───┘ ┴
txt ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ┴ ┴ ┴ └─┘ ┴ └─┘ └─┘ └─┘ └─┘ └─┘ └─┘ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
344 refine is_integral_of_mem_of_fg (adjoin R (S ∪ {comap.to_comap R A B x})) _ _ _,
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
345 swap, { apply subset_adjoin, simp },
st └┘
346 apply fg_trans,
347 { apply fg_adjoin_of_finite, { apply finset.finite_to_set },
st └┘
348 intros x hx,
349 rw [finset.mem_coe, finset.mem_image] at hx,
350 rcases hx with ⟨i, hi, rfl⟩,
351 rcases A_int (p.coeff i) with ⟨q, hq, hqx⟩,
id ┴
typ ┴
352 use [q, hq],
353 replace hqx := congr_arg (to_comap R A B : A → (comap R A B)) hqx,
id ┴ ┴ ┴
typ ┴ ┴ ┴
354 rw alg_hom.map_zero at hqx,
355 convert hqx using 1,
356 symmetry, exact polynomial.hom_eval₂ _ _ _ _ },
st └┘
357 { apply fg_adjoin_singleton_of_integral,
358 exact is_integral_trans_aux _ pmonic hp _ rfl }
st └─
359 end
st ──┘
360
361 /-- If A is an R-algebra all of whose elements are integral over R,
362 and B is an A-algebra all of whose elements are integral over A,
363 then all elements of B are integral over R.-/
364 lemma algebra.is_integral_trans (A_int : ∀ x : A, is_integral R x)(B_int : ∀ x:B, is_integral A x) :
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
365 ∀ x:(comap R A B), is_integral R x :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
366 λ x, is_integral_trans A_int x (B_int x)
id ┴ ┴ ┴
typ ┴ ┴ ┴
367
368 end algebra